\begin{tabbing}
1. \=$f$ : \+
\\[0ex]$\forall$$n$, $a$, $b$:$\mathbb{N}$.
\\[0ex]\{\=$m$:$\mathbb{N}\mid$ \+
\\[0ex]$\forall$$k$:$\mathbb{N}$.
\\[0ex]($a$ = fib($k$))
\\[0ex]$\Rightarrow$ (($k$ $\leq$ 0) $\Rightarrow$ ($b$ = 0))
\\[0ex]$\Rightarrow$ ((0 $<$ $k$) $\Rightarrow$ ($b$ = fib($k$ {-} 1)))
\\[0ex]$\Rightarrow$ ($m$ = fib($n$+$k$))\} 
\-\-\\[0ex]2. $n$ : $\mathbb{N}$
\\[0ex]3. $v$ : $\mathbb{N}$
\\[0ex]4. \=$\forall$$k$:$\mathbb{N}$.\+
\\[0ex](1 = fib($k$)) $\Rightarrow$ (($k$ $\leq$ 0) $\Rightarrow$ (0 = 0)) $\Rightarrow$ ((0 $<$ $k$) $\Rightarrow$ (0 = fib($k$ {-} 1))) $\Rightarrow$ ($v$ = fib($n$+$k$))
\-\\[0ex]5. $f$($n$,1,0) = $v$
\\[0ex]$\vdash$  1 = fib(0)
\end{tabbing}